Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 97.87%. Comparing base (7657a08) to head (230e56a).
⚠️ Report is 1 commits behind head on main.

@@           Coverage Diff            @@
##             main     #805    +/-   ##
========================================
  Coverage   97.86%   97.87%            
========================================
  Files         637      639     +2     
  Lines       69818    70008   +190     
========================================
+ Hits        68325    68517   +192     
+ Misses       1493     1491     -2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Agentic Review Report

Structural Check

Structural Review: model KthLargestMTuple

Structural Completeness

Blacklisted File Check

• PASS — none of the banned generated artifacts are present in the diff.

Build Status

• make test: PASS
• make clippy: PASS

Semantic Review

• evaluate() correctness: OK — for the chosen aggregate-only encoding it returns Sum(1) for qualifying tuples and Sum(0) otherwise.
• dims() correctness: OK — the configuration space matches one coordinate choice per set.
• Size getter consistency: OK — num_sets and total_tuples match the registered complexity expression.
• Canonical example semantics: ISSUE — the new example spec stores one qualifying tuple with value 1, while brute-force solve on the same instance returns Sum(14). The follow-up change in src/unit_tests/example_db.rs suppresses that mismatch instead of resolving it.

Issue Compliance

Summary

• 16/16 structural checks passed
• 6/8 issue compliance checks passed
• docs/paper/reductions.typ:4643 contains a mathematically false NP-completeness claim.
• The linked issue's architectural blocker is still unresolved; the PR works around it by weakening shared example-db optimality checks.
• The canonical example metadata is not actually optimal under the solver semantics for this model.

Quality Check

Quality Review

Design Principles

• DRY: OK — the model implementation itself is straightforward and localized.
• KISS: ISSUE — src/unit_tests/example_db.rs:500-509 changes a global invariant test to accept any aggregate-only config/value pair, which is a workaround for this one model's contract mismatch rather than a local solution.
• HC/LC: ISSUE — the PR introduces a model whose solver/example contract does not fit the existing ModelExampleSpec abstraction, then compensates in shared test infrastructure.

HCI (CLI changed)

• Error messages: OK — the new pred create path gives concrete usage strings.
• Discoverability: ISSUE — the paper tells users to run pred solve kth-largest-m-tuple.json, but the default CLI path fails with No reduction path from KthLargestMTuple to ILP.
• Consistency: ISSUE — the feature is described in yes/no terms via threshold k, but pred solve --solver brute-force returns the raw count Sum(14) instead of the decision answer.
• Least surprise: ISSUE — a user following the new paper example hits a solver error unless they already know to add --solver brute-force.
• Feedback: OK — the failing pred solve command does at least suggest --solver brute-force.

Test Quality

• Naive test detection: ISSUE
  • No CLI regression tests cover KthLargestMTuple despite changes in problemreductions-cli/src/cli.rs and problemreductions-cli/src/commands/create.rs.
  • The new src/unit_tests/example_db.rs fallback stops verifying optimality for aggregate-only models, so the mismatch between canonical example metadata and actual solver behavior is no longer exercised.

Issues

Critical (Must Fix)

• docs/paper/reductions.typ:4643 claims NP-completeness from the m = 2, K = 1 case. That statement is mathematically false and contradicts the linked issue context.
• docs/paper/reductions.typ:4647-4649 documents pred solve kth-largest-m-tuple.json, but the actual command fails on the canonical example with No reduction path from KthLargestMTuple to ILP. Reproduced in the PR worktree.

Important (Should Fix)

• src/unit_tests/example_db.rs:500-509 weakens the global canonical-example contract instead of resolving the fact that this model has no witness-compatible "known optimal configuration".
• The new CLI path in problemreductions-cli/src/commands/create.rs:2371-2402 / problemreductions-cli/src/cli.rs:248 has no dedicated regression tests, which is why the broken documented solve path escaped.

Minor (Nice to Have)

• None beyond the items above.

Summary

• The model implementation is mechanically clean, but the PR still has two user-facing correctness problems: false complexity/classification prose in the paper and a documented solve command that does not work.
• Shared example-db tests were loosened to absorb an abstraction mismatch instead of addressing it directly.
• CLI coverage is missing for the newly added user path.

Agentic Feature Tests

Feature Test Report: problem-reductions

Feature tested: KthLargestMTuple
Profile: ephemeral downstream CLI user
Use Case: follow the new model docs/example, create the canonical instance, inspect it, and solve it from the CLI.
Expected Outcome: the documented commands should work end-to-end and make it clear how to obtain the problem's answer for the example instance.
Verdict: fail
Critical Issues: 1

Summary

Per-Feature Details

KthLargestMTuple

• Role: downstream CLI user following the new model docs and examples.
• What I tried:
  • ./target/debug/pred list | rg KthLargestMTuple
  • ./target/debug/pred show KthLargestMTuple
  • ./target/debug/pred create --example KthLargestMTuple -o /tmp/kth-largest-m-tuple.json
  • ./target/debug/pred solve /tmp/kth-largest-m-tuple.json
  • ./target/debug/pred solve /tmp/kth-largest-m-tuple.json --solver brute-force
  • ./target/debug/pred evaluate /tmp/kth-largest-m-tuple.json --config 2,1,2
• Discoverability: Partial. list and show expose the model, but neither path warns that default solve will fail or that the result is a count rather than the yes/no decision.
• Setup: Worked. No extra setup beyond the built CLI.
• Functionality: Partial. list, show, create --example, manual create, and evaluate all work. Plain solve fails; --solver brute-force succeeds and returns Sum(14).
• Expected vs Actual Outcome: Expected the documented command sequence to work and yield the problem's answer for the example instance. Actual behavior requires a manual solver override, and the successful path returns the raw count (Sum(14)) rather than a yes/no answer based on k.
• Blocked steps: None.
• Friction points: misleading paper command; the CLI output does not apply threshold k, even though the prose definition is phrased as a decision problem.
• Doc suggestions: either document pred solve ... --solver brute-force explicitly (and explain that solve returns the qualifying-tuple count), or teach the default solver path how to handle this aggregate-only model.

Issues Found

• confirmed / high severity: pred solve /tmp/kth-largest-m-tuple.json fails on the canonical example, despite the new paper entry documenting exactly that command. Workaround: --solver brute-force.
• confirmed / medium severity: the user-facing solve result is Sum(14) rather than the thresholded yes/no answer implied by the problem statement and the k field.

Generated by review-pipeline

Follow-up items (recorded during final review):

• Improve model_specs_are_optimal test: add supports_witnesses flag and reject large search spaces #895 — Improve model_specs_are_optimal test: add supports_witnesses flag to VariantEntry, reject large canonical examples, and restructure the three-way branch